SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Semantics encoding</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Semantics encoding</span></span>

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

<p>A <b>semantics encoding</b> is a translation between <a href="Formal_language" title="Formal language">formal languages</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> For programmers, the most familiar form of encoding is the compilation of a programming language into <a href="Machine_code" title="Machine code">machine code</a> or <a href="Bytecode" title="Bytecode">byte-code</a>. Conversion between document formats are also forms of encoding. Compilation of <a href="TeX" title="TeX">TeX</a> or <a href="LaTeX" title="LaTeX">LaTeX</a> documents to <a href="PostScript" title="PostScript">PostScript</a> are also commonly encountered encoding processes. Some high-level preprocessors, such as <a href="OCaml" title="OCaml">OCaml</a>'s <a href="Camlp4" title="Camlp4">Camlp4</a>, also involve encoding of a programming language into another.

</p><p>Formally, an encoding of a language A into language B is a mapping of all terms of A into B. If there is a <i>satisfactory</i> encoding of A into B, B is considered <i>at least as powerful</i> (or <i>at least as expressive</i>) as A.

</p>

<div class="mw-heading mw-heading2"><h2 id="Properties">Properties</h2></div>

<p>An informal notion of translation is not sufficient to help determine expressivity of languages, as it permits trivial encodings such as mapping all elements of A to the same element of B. Therefore, it is necessary to determine the definition of a "good enough" encoding. This notion varies with the application.

</p><p>Commonly, an encoding <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [\cdot ]:A\longrightarrow B}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [\cdot ]:A\longrightarrow B}</annotation>

</semantics>

</math></span><img src="./19aca89d1b15088ab5ddecd85ec90ab13edac688.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:12.481ex; height:2.843ex;" alt="{\displaystyle [\cdot ]:A\longrightarrow B}" loading="lazy"></span> is expected to preserve a number of properties.

</p>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_compositions">Preservation of compositions</h3></div>

<dl><dt>soundness</dt>

<dd>For every n-ary operator <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle op_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle op_{A}}</annotation>

</semantics>

</math></span><img src="./1e5295a09ebff10fba9b4e8173210ea19b247716.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.762ex; height:2.009ex;" alt="{\displaystyle op_{A}}" loading="lazy"></span> of A, there exists an n-ary operator <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle op_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle op_{B}}</annotation>

</semantics>

</math></span><img src="./22eab80d8707868ea1b4e633f91e62e7aa9e86f8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.777ex; height:2.009ex;" alt="{\displaystyle op_{B}}" loading="lazy"></span> of B such that</dd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \forall T_{A}^{1},T_{A}^{2},\dots ,T_{A}^{n},[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})]=op_{B}([T_{A}^{1}],[T_{A}^{2}],\cdots ,[T_{A}^{n}])}</annotation>

</semantics>

</math></span><img src="./dde845e5d034bd6a375773b70e51b3c59c212dbe.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:66.143ex; height:3.176ex;" alt="{\displaystyle \forall T_{A}^{1},T_{A}^{2},\dots ,T_{A}^{n},[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})]=op_{B}([T_{A}^{1}],[T_{A}^{2}],\cdots ,[T_{A}^{n}])}" loading="lazy"></span></dd>

<dt>completeness</dt>

<dd>For every n-ary operator <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle op_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle op_{A}}</annotation>

</semantics>

</math></span><img src="./1e5295a09ebff10fba9b4e8173210ea19b247716.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.762ex; height:2.009ex;" alt="{\displaystyle op_{A}}" loading="lazy"></span> of A, there exists an n-ary operator <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle op_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle op_{B}}</annotation>

</semantics>

</math></span><img src="./22eab80d8707868ea1b4e633f91e62e7aa9e86f8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.777ex; height:2.009ex;" alt="{\displaystyle op_{B}}" loading="lazy"></span> of B such that</dd>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

<msub>

</mrow>

</msub>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \forall T_{B}^{1},T_{B}^{2},\dots ,T_{B}^{n},\exists T_{A}^{1},\dots ,T_{A}^{n},op_{B}(T_{B}^{1},\cdots ,T_{B}^{N})=[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})]}</annotation>

</semantics>

</math></span><img src="./74cef38c88f773bd4701bb12fe05cd449137b073.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:72.188ex; height:3.176ex;" alt="{\displaystyle \forall T_{B}^{1},T_{B}^{2},\dots ,T_{B}^{n},\exists T_{A}^{1},\dots ,T_{A}^{n},op_{B}(T_{B}^{1},\cdots ,T_{B}^{N})=[op_{A}(T_{A}^{1},T_{A}^{2},\cdots ,T_{A}^{n})]}" loading="lazy"></span></dd></dl>

<p>(Note: as far as the author is aware of, this criterion of completeness is never used.)

</p><p>Preservation of compositions is useful insofar as it guarantees that components can be examined either separately or together without "breaking" any interesting property. In particular, in the case of compilations, this soundness guarantees the possibility of proceeding with separate compilation of components, while completeness guarantees the possibility of de-compilation.

</p>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_reductions">Preservation of reductions</h3></div>

<p>This assumes the existence of a notion of reduction on both language A and language B. Typically, in the case of a programming language, reduction is the relation which models the execution of a program.

</p><p>We write <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \longrightarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \longrightarrow }</annotation>

</semantics>

</math></span><img src="./4ffb6a294b21bebe64570c4088d77a884dec95ab.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.806ex; height:1.843ex;" alt="{\displaystyle \longrightarrow }" loading="lazy"></span> for one step of reduction and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \longrightarrow ^{*}}">

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \longrightarrow ^{*}}</annotation>

</semantics>

</math></span><img src="./cd9a60098d34b7f09c79208e4528abea1fefa305.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:4.86ex; height:2.343ex;" alt="{\displaystyle \longrightarrow ^{*}}" loading="lazy"></span> for any number of steps of reduction.

</p>

<dl><dt>soundness</dt>

<dd>For every terms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1},T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1},T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./410d7f605ad5dc197ad04e9482c29b1dbce72de4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.679ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1},T_{A}^{2}}" loading="lazy"></span> of language A, if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

<msup>

</mrow>

</msup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./950ddb2156a728f848344809b952025949a9dd2e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:11.795ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}\longrightarrow ^{*}T_{A}^{2}}" loading="lazy"></span> then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

<msup>

</mrow>

</msup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./bde01dedfc92724d76f941c790c7f599b1798761.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:14.382ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]\longrightarrow ^{*}[T_{A}^{2}]}" loading="lazy"></span>.</dd>

<dt>completeness</dt>

<dd>For every term <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}}</annotation>

</semantics>

</math></span><img src="./9575caccd68779781e5357ffe2c14d0d37404183.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}}" loading="lazy"></span> of language A and every terms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{B}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{B}^{2}}</annotation>

</semantics>

</math></span><img src="./67d6bc7173400650c58c5921dd12d6059c767099.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.837ex; height:3.176ex;" alt="{\displaystyle T_{B}^{2}}" loading="lazy"></span> of language B, if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}}">

</mrow>

</mrow>

</msubsup>

<msup>

</mrow>

</msup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}}</annotation>

</semantics>

</math></span><img src="./9dd667979eebd6866eee648229515da4e538baf0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:13.103ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]\longrightarrow ^{*}T_{B}^{2}}" loading="lazy"></span> then there exists some <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./1a5854ad09402b2e6da2a35f50be5224457350a9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{2}}" loading="lazy"></span> such that <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{B}^{2}=[T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{B}^{2}=[T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./96f3d79a7978ba1f707a8d9ad6c3cd9a6ec58bdd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.052ex; height:3.176ex;" alt="{\displaystyle T_{B}^{2}=[T_{A}^{2}]}" loading="lazy"></span>.</dd></dl>

<p>This preservation guarantees that both languages behave the same way. Soundness guarantees that all possible behaviours are preserved while completeness guarantees that no behaviour is added by the encoding. In particular, in the case of compilation of a programming language, soundness and completeness together mean that the compiled program behaves accordingly to the high-level semantics of the programming language.

</p>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_termination">Preservation of termination</h3></div>

<p>This also assumes the existence of a notion of reduction on both language A and language B.

</p>

<dl><dt>soundness</dt>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}}</annotation>

</semantics>

</math></span><img src="./416a1dd7d799d8a81370d796e350420774dc2369.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.822ex; height:2.509ex;" alt="{\displaystyle T_{A}}" loading="lazy"></span>, if all reductions of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}}</annotation>

</semantics>

</math></span><img src="./416a1dd7d799d8a81370d796e350420774dc2369.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.822ex; height:2.509ex;" alt="{\displaystyle T_{A}}" loading="lazy"></span> converge, then all reductions of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}]}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span> converge.</dd>

<dt>completeness</dt>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span>, if all reductions of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}]}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span> converge, then all reductions of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}}</annotation>

</semantics>

</math></span><img src="./416a1dd7d799d8a81370d796e350420774dc2369.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.822ex; height:2.509ex;" alt="{\displaystyle T_{A}}" loading="lazy"></span> converge.</dd></dl>

<p>In the case of compilation of a programming language, soundness guarantees that the compilation does not introduce non-termination such as endless loops or endless recursions. The completeness property is useful when language B is used to study or test a program written in language A, possibly by extracting key parts of the code: if this study or test proves that the program terminates in B, then it also terminates in A.

</p>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_observations">Preservation of observations</h3></div>

<p>This assumes the existence of a notion of observation on both language A and language B. In programming languages, typical observables are results of inputs and outputs, by opposition to pure computation. In a description language such as <a href="HTML" title="HTML">HTML</a>, a typical observable is the result of page rendering.

</p>

<dl><dt>soundness</dt>

<dd>for every observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{A}}</annotation>

</semantics>

</math></span><img src="./e883292332321eab29bd5c8e348ca678e7120bba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.68ex; height:2.509ex;" alt="{\displaystyle obs_{A}}" loading="lazy"></span> on terms of A, there exists an observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{B}}</annotation>

</semantics>

</math></span><img src="./f9237cea9654453882d20aee9992180d450aa0af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.695ex; height:2.509ex;" alt="{\displaystyle obs_{B}}" loading="lazy"></span> of terms of B such that for any term <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}}</annotation>

</semantics>

</math></span><img src="./416a1dd7d799d8a81370d796e350420774dc2369.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.822ex; height:2.509ex;" alt="{\displaystyle T_{A}}" loading="lazy"></span> with observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{A}}</annotation>

</semantics>

</math></span><img src="./e883292332321eab29bd5c8e348ca678e7120bba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.68ex; height:2.509ex;" alt="{\displaystyle obs_{A}}" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}]}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span> has observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{B}}</annotation>

</semantics>

</math></span><img src="./f9237cea9654453882d20aee9992180d450aa0af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.695ex; height:2.509ex;" alt="{\displaystyle obs_{B}}" loading="lazy"></span>.</dd>

<dt>completeness</dt>

<dd>for every observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{A}}</annotation>

</semantics>

</math></span><img src="./e883292332321eab29bd5c8e348ca678e7120bba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.68ex; height:2.509ex;" alt="{\displaystyle obs_{A}}" loading="lazy"></span> on terms of A, there exists an observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{B}}</annotation>

</semantics>

</math></span><img src="./f9237cea9654453882d20aee9992180d450aa0af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.695ex; height:2.509ex;" alt="{\displaystyle obs_{B}}" loading="lazy"></span> on terms of B such that for any term <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}]}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span> with observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{B}}</annotation>

</semantics>

</math></span><img src="./f9237cea9654453882d20aee9992180d450aa0af.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.695ex; height:2.509ex;" alt="{\displaystyle obs_{B}}" loading="lazy"></span>, <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}}</annotation>

</semantics>

</math></span><img src="./416a1dd7d799d8a81370d796e350420774dc2369.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.822ex; height:2.509ex;" alt="{\displaystyle T_{A}}" loading="lazy"></span> has observable <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle obs_{A}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle obs_{A}}</annotation>

</semantics>

</math></span><img src="./e883292332321eab29bd5c8e348ca678e7120bba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.68ex; height:2.509ex;" alt="{\displaystyle obs_{A}}" loading="lazy"></span>.</dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_simulations">Preservation of simulations</h3></div>

<p>This assumes the existence of notion of simulation on both language A and language B. In a programming languages, a program simulates another if it can perform all the same (observable) tasks and possibly some others. Simulations are used typically to describe compile-time optimizations.

</p>

<dl><dt>soundness</dt>

<dd>for every terms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1},T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1},T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./410d7f605ad5dc197ad04e9482c29b1dbce72de4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.679ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1},T_{A}^{2}}" loading="lazy"></span>, if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./1a5854ad09402b2e6da2a35f50be5224457350a9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{2}}" loading="lazy"></span> simulates <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}}</annotation>

</semantics>

</math></span><img src="./9575caccd68779781e5357ffe2c14d0d37404183.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}}" loading="lazy"></span> then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./b10b70a9345937b25c131ee5f77e12da11b6b338.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{2}]}" loading="lazy"></span> simulates <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]}</annotation>

</semantics>

</math></span><img src="./be9ac18028afcf0dd1fc2b7a35f5b1320b2a8029.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]}" loading="lazy"></span>.</dd>

<dt>completeness</dt>

<dd>for every terms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1},T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1},T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./410d7f605ad5dc197ad04e9482c29b1dbce72de4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:6.679ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1},T_{A}^{2}}" loading="lazy"></span>, if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./b10b70a9345937b25c131ee5f77e12da11b6b338.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{2}]}" loading="lazy"></span> simulates <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]}</annotation>

</semantics>

</math></span><img src="./be9ac18028afcf0dd1fc2b7a35f5b1320b2a8029.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]}" loading="lazy"></span> then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./1a5854ad09402b2e6da2a35f50be5224457350a9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{2}}" loading="lazy"></span> simulates <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}}</annotation>

</semantics>

</math></span><img src="./9575caccd68779781e5357ffe2c14d0d37404183.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}}" loading="lazy"></span>.</dd></dl>

<p>Preservation of simulations is a much stronger property than preservation of observations, which it entails. In turn, it is weaker than a property of preservation of <a href="Bisimulation" title="Bisimulation">bisimulations</a>. As in previous cases, soundness is important for compilation, while completeness is useful for testing or proving properties.

</p>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_equivalences">Preservation of equivalences</h3></div>

<p>This assumes the existence of a notion of equivalence on both language A and language B. Typically, this can be a notion of equality of structured data or a notion of syntactically different yet semantically identical programs, such as structural congruence or structural equivalence.

</p>

<dl><dt>soundness</dt>

<dd>if two terms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}}</annotation>

</semantics>

</math></span><img src="./9575caccd68779781e5357ffe2c14d0d37404183.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./1a5854ad09402b2e6da2a35f50be5224457350a9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{2}}" loading="lazy"></span> are equivalent in A, then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]}</annotation>

</semantics>

</math></span><img src="./be9ac18028afcf0dd1fc2b7a35f5b1320b2a8029.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./b10b70a9345937b25c131ee5f77e12da11b6b338.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{2}]}" loading="lazy"></span> are equivalent in B.</dd>

<dt>completeness</dt>

<dd>if two terms <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]}</annotation>

</semantics>

</math></span><img src="./be9ac18028afcf0dd1fc2b7a35f5b1320b2a8029.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./b10b70a9345937b25c131ee5f77e12da11b6b338.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:4.116ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{2}]}" loading="lazy"></span> are equivalent in B, then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}}</annotation>

</semantics>

</math></span><img src="./9575caccd68779781e5357ffe2c14d0d37404183.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./1a5854ad09402b2e6da2a35f50be5224457350a9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:2.822ex; height:3.176ex;" alt="{\displaystyle T_{A}^{2}}" loading="lazy"></span> are equivalent in A.</dd></dl>

<div class="mw-heading mw-heading3"><h3 id="Preservation_of_distribution">Preservation of distribution</h3></div>

<p>This assumes the existence of a notion of distribution on both language A and language B. Typically, for compilation of distributed programs written in Acute, <a href="JoCaml" title="JoCaml">JoCaml</a> or E, this means distribution of processes and data among several computers or CPUs.

</p>

<dl><dt>soundness</dt>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}}</annotation>

</semantics>

</math></span><img src="./416a1dd7d799d8a81370d796e350420774dc2369.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.822ex; height:2.509ex;" alt="{\displaystyle T_{A}}" loading="lazy"></span> is the composition of two agents <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}~|~T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}~|~T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./c600662d1e635b029d9e7255375aad43adb497a8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.453ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}~|~T_{A}^{2}}" loading="lazy"></span> then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}]}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span> must be the composition of two agents <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}</annotation>

</semantics>

</math></span><img src="./784f00992a928772e56b029bf1728385de1feb82.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.04ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]~|~[T_{A}^{2}]}" loading="lazy"></span>.</dd>

<dt>completeness</dt>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}]}</annotation>

</semantics>

</math></span><img src="./a087d69201a7b416bb74bf1b3fb8e1831a58fb7e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:4.116ex; height:2.843ex;" alt="{\displaystyle [T_{A}]}" loading="lazy"></span> is the composition of two agents <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{B}^{1}~|~T_{B}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{B}^{1}~|~T_{B}^{2}}</annotation>

</semantics>

</math></span><img src="./f7cb61c58355cce364b6f0d052d8c449adf15fe4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.482ex; height:3.176ex;" alt="{\displaystyle T_{B}^{1}~|~T_{B}^{2}}" loading="lazy"></span> then <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{B}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{B}}</annotation>

</semantics>

</math></span><img src="./b558df0361c34c9e93a63042e0d01b44e0295cc0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.837ex; height:2.509ex;" alt="{\displaystyle T_{B}}" loading="lazy"></span> must be the composition of two agents <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T_{A}^{1}~|~T_{A}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T_{A}^{1}~|~T_{A}^{2}}</annotation>

</semantics>

</math></span><img src="./c600662d1e635b029d9e7255375aad43adb497a8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:7.453ex; height:3.176ex;" alt="{\displaystyle T_{A}^{1}~|~T_{A}^{2}}" loading="lazy"></span> such that <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{1}]=T_{B}^{1}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{1}]=T_{B}^{1}}</annotation>

</semantics>

</math></span><img src="./089444c5859c1fb8e17194f0589836fd5275f903.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.052ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{1}]=T_{B}^{1}}" loading="lazy"></span> and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle [T_{A}^{2}]=T_{B}^{2}}">

</mrow>

</mrow>

</msubsup>

</mrow>

</mrow>

</msubsup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle [T_{A}^{2}]=T_{B}^{2}}</annotation>

</semantics>

</math></span><img src="./b317ae33635167dae14a8a6da01e0e5f0b301814.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -1.005ex; width:10.052ex; height:3.176ex;" alt="{\displaystyle [T_{A}^{2}]=T_{B}^{2}}" loading="lazy"></span>.</dd></dl>

<ul><li><a href="Bisimulation" title="Bisimulation">Bisimulation</a></li>

<li><a href="Compiler" title="Compiler">Compiler</a></li>

<li><a href="Semantics" title="Semantics">Semantics</a></li>

<li><a href="Semantic_dictionary_encoding" title="Semantic dictionary encoding">Semantic dictionary encoding</a> (SDE)</li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFvan_Glabbeek2018" class="citation cs2">van Glabbeek, Rob (2018), <a rel="nofollow" class="external text" href="https://doi.org/10.1007/978-3-319-89366-2_10">"A Theory of Encodings and Expressiveness (Extended Abstract)"</a>, <i>Lecture Notes in Computer Science</i>, Cham: Springer International Publishing, pp. <span class="nowrap">183–</span>202, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-319-89365-5</bdi><span class="reference-accessdate">, retrieved <span class="nowrap">2025-07-19</span></span></cite></span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.program-transformation.org/">The Program Transformation Wiki</a></li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-19" href="https://en.wikipedia.org/wiki/?title=Semantics_encoding&oldid=1301409597">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>